%%% PDF functionality.

\usepackage[pdftex]{hyperref}
%\usepackage{pdfcomment}

%%% Layout and design.

\usepackage[T1]{fontenc}
\usepackage{textcomp}
\usepackage{microtype}

\usepackage{times}
\usepackage[scaled]{berasans}
\usepackage[scaled]{beramono}

\usepackage[small,compact]{titlesec}
\usepackage[usenames,dvipsnames,svgnames,x11names]{xcolor}

% PDF link colors
% The color values and names come from the Tango Icon Scheme
\definecolor{SkyBlue2}{rgb}{.204, .396, .643}
\definecolor{ScarletRed3}{rgb}{.643, 0, 0}
\definecolor{Chocolate3}{rgb}{.561, .349, .008}

\hypersetup{%
  % Color the text of links instead of framing them.
  colorlinks=true,
  linkcolor=SkyBlue2,
  urlcolor=ScarletRed3,
  filecolor=Chocolate3
}

%%% Additional symbols and notation.

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{stmaryrd}

%%% Graphics.

\usepackage{tikz}
\usetikzlibrary{shapes.misc}
\usetikzlibrary{calc}

%%% Auxiliary packages.

\usepackage{calc}
\usepackage{ifthen}
\usepackage{ifdraft}
\usepackage{ucs}
\usepackage{xspace}



%\makeatletter

% Page Setup %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% To output all definitions, rules, and comments onto a single, long page, we
% take the following steps:
%
% - Wrap the whole document in a 'kdefinition' environment and tell the
%   'preview' package to typeset it onto a single page.  This gives us a single
%   page of output.  Setting a suitable border and the 'tightpage' option
%   adjusts the page height to match the content.
%
% - Finding the correct page width requires two runs of TeX[1].  In the first
%   run, we mark the width of every typeset block (rules, comments, etc.).
%   This information is is written into an auxiliary file of name
%   '\jobname.mrk'.  At the beginning of the second run, we read this file
%   (if it exists), determine the maximum width, and use the maximum as
%   the text width.  If no width information is available, we default to
%   a text width of 16 inches.
%
% ---
% [1] (At least) two runs are necessary anyway: cross-referencing and indexing
%     require them, and so do PDF annotations.

%\pagestyle{empty}

%%% PDF default view

% Most PDF viewers seem to default to the "fit whole page" view mode.  A single,
% long page badly fits this behavior, so we request "fit page width" instead.
\hypersetup{pdfstartview=FitH}

%%% Use the 'preview' package to typeset everything onto a single page.

%\usepackage[active,tightpage,pdftex]{preview}
%\setlength\PreviewBorder{5pt}

% Everything within an environment that is marked as \PreviewEnvironment
% is put onto its own page.  Thus, by defining a global environment that
% wraps the whole document, we get all output on a single page.
%
% The 'kompile.pl' script takes care of the wrapping.
\newenvironment{kdefinition}{}{}
%\PreviewEnvironment{kdefinition}


%%% Determine the text width from markers put at the lower right end of
%   each content block.

% The system layer of the 'PGF' package hides the gory details.
% (See "Position Tracking Commands" in Part XIII of the PGF manual.)
%\usepackage{pgfsys}

% Try to load the marker positions from the previous run.
%\newcounter{k@prevMarkerCount}%
%\InputIfFileExists{\jobname.mrk}{}{}%

% Set the text width to the maximum of the X coordinates.
%\newlength{\k@maxX}%
%\newlength{\k@currentMarkerX}%
%
%\whiledo{\value{k@prevMarkerCount} > 0}{%
%  \addtocounter{k@prevMarkerCount}{-1}%
%  \pgfsys@getposition{k@marker@\the\c@k@prevMarkerCount}{\k@currentMarker}%
%  \pgfextractx{\k@currentMarkerX}{\k@currentMarker}%
%    \ifthenelse{\lengthtest{\k@currentMarkerX > \k@maxX}}{%
%      \setlength{\k@maxX}{\k@currentMarkerX}%
%    }{}%
%}%
%\ifthenelse{\lengthtest{\k@maxX > 0pt}}{%
%  \setlength{\textwidth}{\k@maxX}%
%}{%
%  \setlength{\textwidth}{16in}%
%}%


% To mark the position, we use the PGF system layer macro \pgfsys@markposition.
% However, this macro usually writes to the main auxiliary file '\jobname.aux'.
% This will not work in our setting because the marker positions would then
% only be available just before the document starts, which is too late to set
% the text width.  Thus we use our own auxiliary file.

% Open the marker file for writing.
%\newwrite\k@markerOut
%\immediate\openout\k@markerOut=\jobname.mrk

%\newcounter{k@marker}
% The marker macro generates the marker names and briefly swaps the output
% stream that \pgfsys@markposition uses before calling it.
%\newcommand{\k@markPosition}{%
%  \let\k@tmpAuxOut=\pgfutil@auxout%
%  \let\pgfutil@auxout=\k@markerOut%
%  \pgfsys@markposition{k@marker@\the\c@k@marker}%
%  \let\pgfutil@auxout=\k@tmpAuxOut%
%  \addtocounter{k@marker}{1}%
%}

% Also store the number of set markers for the next run (for easier looping).
%\AtEndDocument{%
%  \immediate\write\k@markerOut{%
%    \string\setcounter{k@prevMarkerCount}{\the\c@k@marker}%
%  }{}%
%}


% Title %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\renewcommand{\@maketitle}{
% \null
% \vspace*{3ex}
% {\Huge \@title}
% \par\vspace*{2ex}
% {\Large \@author}
% \par\vspace*{1ex}
% {\large \@organization}
% \par\vspace*{3ex}
%}

% Also add respective PDF meta information
\hypersetup{
  pdftitle={\@title},
  pdfauthor={\@author}
}

\let\k@oldTitle=\title
\renewcommand{\title}[1]{%
  \k@oldTitle{#1}%
  \hypersetup{pdftitle={#1}}%
}
\let\k@oldAuthor=\author
\renewcommand{\author}[1]{%
  \k@oldAuthor{#1}%
  \hypersetup{pdfauthor={#1}}%
}
\let\@organization=\@empty
\newcommand{\organization}[1]{%
  \def\@organization{#1}%
}


% Source Comments %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Turn off section numbering: all headings will look like they were starred.
% However, they will still appear in the table of contents (and the bookmarks
% that hyperref generates for the PDF).
%
% Note that hyperref seems to rely on the "secnumdepth" counter for bookmark
% generation.  Thus, the "traditional" approach \setcounter{secnumdepth}{0}
% leads to (rather) arbitrary bookmark nestings.
%
% Simply remove the labeling number from all titles.
\titlelabel{}
% Create TOC entries down to subsections.
\setcounter{tocdepth}{4}
% Show the TOC by default.
\hypersetup{%
  bookmarksopen=true,
  bookmarksopenlevel=2
}

\usepackage{fancyvrb}
\usepackage{fancybox}

\tikzset{comment/.style={
    rectangle,
    rounded corners,
    draw,
    fill=white!10,
    inner sep=.75em
  }
}

% The comment environment.
\newenvironment{latexComment}{%
\par
  \begin{Sbox}%
    \begin{minipage}{\textwidth}%
      \addtolength{\parskip}{.5\baselineskip}%
}{%
    \end{minipage}%
  \end{Sbox}%
  \bigskip%
  \begin{tikzpicture}
    \node[comment]{\TheSbox};
  \end{tikzpicture}%
%  \k@markPosition%
  \medskip%
}

% Macros for use in the comments.
\newcommand{\K}{\mbox{$\mathbb{K}$}\xspace}
\newcommand{\KLabel}{\textit{KLabel}\xspace}
\newcommand{\KResult}{\textit{KResult}\xspace}


% Special Glyphs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\lp}{(}
\newcommand{\rp}{)}
\newcommand{\myquote}[1]{\text{\rmfamily ``\ttfamily #1\rmfamily ''}}

\newcommand{\mysinglequote}[1]{\text{\rmfamily "}}
\newcommand{\mybracket}[1]{(#1)}
\newcommand{\sqbracket}[1]{[#1]}
\newcommand{\crlbracket}[1]{{#1}}

\newcommand{\nothing}{}
\newcommand{\somespace}{\mathbin{}}
\newcommand{\subscript}[1]{\ensuremath{\nothing_{#1}}}

\newcommand{\kLarge}[1]{\left(\begin{array}{@{}c@{}}#1\end{array}\right)}
\newcommand{\kBR}{\\}


% Modules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{module}[1]{%
  \par\noindent%
  \text{\scshape Module #1}%
  \setlength{\parindent}{1em}%
}{%
  \par\noindent\text{\scshape end module}%
  \vspace{3ex}
}
\newcommand{\moduleName}[1]{#1}
\newcommand{\including}[1]{\par\text{\scshape imports}\ #1}
\newcommand{\modulePlus}{$+$}


% Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Sorts and kinds.
\newcommand{\sorts}[1]{}
\newcommand{\sort}[1]{\text{\itshape #1}}
\newcommand{\kind}[1]{\text{\itshape #1}}

% Syntax rules.
\newlength{\syntaxlength}  % The amount of indention for continued rules.

\newcommand{\syntax}[3]{\par\indent%
\hbox{%
\mbox{\scshape syntax}\hspace{1em}$#1\mathrel{::=}{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]}%
}%\k@markPosition%
}
\newcommand{\syntaxCont}[3]{\par\indent%
\hbox{%
  $\setlength{\syntaxlength}{\widthof{$\mathrel{::=}$}}%
  \setlength{\syntaxlength}{.5\syntaxlength}%
  \addtolength{\syntaxlength}{\widthof{\mbox{\scshape syntax}\hspace{1em}$#1$}}%
  \hspace{\syntaxlength}%
  \;\;\!\mid\;{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]}%
  }%\k@markPosition%
}

% Non-terminals.
\newcommand{\nonTerminal}[1]{\text{\itshape #1}\/}

% Terminals.
\newcommand{\terminal}[1]{\ensuremath\mathrel{\text{\ttfamily #1}}}
\newcommand{\terminalNoSpace}[1]{\ensuremath\mathord{\text{\ttfamily #1}}}

% Tags.
\newcommand{\kassoc}{assoc}
\newcommand{\kcomm}{comm}
\newcommand{\khybrid}{{\color{blue}hybrid}}
\newcommand{\kid}[1]{id: {#1}}
\newcommand{\kditto}{ditto}
\newcommand{\karity}[1]{{\color{blue}arity(#1)}}
\newcommand{\kstrict}[2]{{%
  \color{blue}strict%
  \ifx&#1&%
  \else%
    (#1)%
  \fi%
  \ifx&#2&%
  \else%
    in (#2)%
  \fi%
}}
\newcommand{\kseqstrict}[2]{{%
  \color{blue}seqstrict%
  \ifx&#1&%
  \else%
    (#1)%
  \fi%
  \ifx&#2&%
  \else%
    in (#2)%
  \fi%
}}


% Configuration %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\kconfig}[2][]{\par%
  {\sc configuration:}%
  \begin{quote}
    \par#1\hbox{\ensuremath{\begin{array}[t]{@{}c@{}}#2\end{array}}}%	\k@markPosition%
  \end{quote}%
}


% Cells %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\cellDecl}[2]{\par%
  \text{\scshape cell:} $#1$ wraps $#2$%
}

%%% Tooltips.

% Following a how-to guide for Adobe InDesign, we create tooltips for items by
% overlaying them with a transparent button.
%
% For documentation on the JavaScript objects, see the JavaScript for Acrobat
% API Reference at http://www.adobe.com/devnet/acrobat/javascript.html
%
% For documentation on the PDF code, see the PDF reference manual at
% http://www.adobe.com/devnet/pdf/pdf_reference.html

% These definitions will hold the payload.  They have to be global because
% hyperref definitions vanish when the document starts(?).
\def\k@tooltipText{}%
\edef\k@tooltipString{}%

% The "user name" of fields is the user visible name of this entity.  For
% (non-readonly) buttons, it shows up as tooltip when the mouse hovers over it.
% Unfortunately, the hyperref package does not allow specifying the user name;
% thus, by means of a small hack, we push in some raw PDF code when hyperref
% creates a PushButton object.  The raw PDF code is appended to the "flags"
% field \Fld@flags.  See the button creation macro "\PDFForm@Push" in the
% hpdftex.def driver.
%
% For the definition of the user name property of fields, see section 12.7.3.1
% in the PDF specification.
\let\k@hyPushButtonFlags=\HyField@FlagsPushButton
\gdef\HyField@FlagsPushButton{%
  % Execute the original macro
  \k@hyPushButtonFlags%
  % Save the current flags and add the user visible name via /TU ("text user"?).
  \let\k@currentFlags=\Fld@flags%
  \pdfstringdef\k@tooltipString{\k@tooltipText}%
  \edef\Fld@flags{/TU (\k@tooltipString)\k@currentFlags}%
  \edef\Fld@bordercolor{\space}%
}

\newcounter{k@tooltipCounter}

\newcommand{\k@withTooltip}[2]{%
  % #1 is the target / box, #2 is the tooltip
  \def\k@tooltipText{#2}
  \hbox{\PushButton[name=tooltip\the\c@k@tooltipCounter,
              borderwidth=0,
              % The focus handler executes before the click happens, so the
              % button is set to "not interact" just before it would change
              % its visual appearance.
              onfocus={ var t = this.getField("tooltip\the\c@k@tooltipCounter");
                       t.highlight = highlight.n; }
             ]{#1}}%
  \addtocounter{k@tooltipCounter}{1}%
}

% Buttons are form elements and require a surrounding Form environment.
% \AtBeginDocument{\begin{Form}}
% \AtEndDocument{\end{Form}}

%%% Cell contents.

\newcommand{\reduceTop}[2]{{#1}\Rightarrow{#2}}
\newcommand{\reduceTopS}[2]{{#1}\rightharpoonup{#2}}
\newcommand{\reduce}[2]{\hbox{%
  \begin{tikzpicture}[baseline=(top.base),
                      inner xsep=0pt,
                      inner ysep=.3333ex,
                      minimum width=2em]
    \path node (top) {$#1$\strut}
          (top.south)
          node (bottom) [anchor=north, inner ysep=.5ex] {$#2$\strut};
    %%% Draw the horizontal line:
    % Line with chevron.
    %\path[draw,thin,solid] let \p1 = (current bounding box.west),
    %                           \p2 = (current bounding box.east),
    %                           \p3 = (top.south)
    %                       in (top.south) ++(0,-1.5pt) -- ++(-2pt,1.5pt) -- (\x1,\y3)
    %                          (top.south) ++(0,-1.5pt) -- ++(2pt,1.5pt)  -- (\x2,\y3);
    %%% Other options:
    % Solid line.
    \path[draw,thin,solid] let \p1 = (current bounding box.west),
                               \p2 = (current bounding box.east),
                               \p3 = (top.south)
                           in (\x1,\y3) -- (\x2,\y3);
    % Solid arrow (augmenting the solid line).
    \path[fill] (top.south) ++(2pt,0) -- ++(-4pt,0) -- ++(2pt,-1.5pt) -- cycle;
  \end{tikzpicture}%
}}
\newcommand{\reduceS}[2]{\hbox{%
  \begin{tikzpicture}[baseline=(top.base),
                      inner xsep=0pt,
                      inner ysep=.3333ex,
                      minimum width=2em]
    \path node (top) {$#1$\strut}
          (top.south)
          node (bottom) [anchor=north] {$#2$\strut};
    \path[draw,thin,densely dashed] let \p1 = (current bounding box.west),
                                        \p2 = (current bounding box.east),
                                        \p3 = (top.south)
                                    in (\x1,\y3) -- (\x2,\y3);
  \end{tikzpicture}%
}}
\newcommand{\kra}{\curvearrowright}
\newcommand{\kvalue}[1]{{\color{red}#1}}
\newcommand{\constant}[2]{%
  \k@withTooltip{\text{\sffamily #1}}{Constant Sort: #2}%
}
\newcommand{\variable}[2]{%
  \k@withTooltip{\text{\itshape #1}\/}{Variable Sort: #2}%
}

\newcommand{\displayGreek}[1]{%
  \text{\Large\ensuremath{\displaystyle #1}}%
}

\newcommand{\prefixOp}[1]{\text{\sffamily #1}}
\newcommand{\dotCt}[1]{%
  \k@withTooltip{\raise.3ex\hbox{\ensuremath{\kdot}}}{Constant Sort: #1}%
}

%%% Mathematical notation.

\newcommand{\mall}[3]{\langle{#3}\rangle_{\sf #2}}
\newcommand{\mallLarge}[3]{\left\langle\begin{array}{c}#3\end{array}\right\rangle_{{\sf #2}}}
\newcommand{\ellipses}{\mathrel{\cdot\!\!\cdot\!\!\cdot}}
\newcommand{\mprefix}[3]{\mall{#1}{#2}{{#3}\ \ellipses}}
\newcommand{\msuffix}[3]{\mall{#1}{#2}{\ellipses\ {#3}}}
\newcommand{\mmiddle}[3]{\mall{#1}{#2}{\ellipses\ {#3}\ \ellipses}}
\newcommand{\mdot}{\cdot}
\newcommand{\mAnyVar}[1]{\_}

%%% Bubble notation.

\newcommand{\ball}[3]{\kcell{#1}{#2}{$#3$}{convex}{convex}}
\newcommand{\bLarge}[5]{%
  \kcell{#1}%
        {#2}%
        {$\begin{array}[t]{@{}c@{}}%
            #3%
          \end{array}$}%
        {#4}%
        {#5}%
}

\newcommand{\ballLarge}[3]{\bLarge{#1}{#2}{#3}{convex}{convex}}                                                                 
\newcommand{\bprefixLarge}[3]{\bLarge{#1}{#2}{#3}{convex}{none}}                                                                
\newcommand{\bsuffixLarge}[3]{\bLarge{#1}{#2}{#3}{none}{convex}}                                                                
\newcommand{\bmiddleLarge}[3]{\bLarge{#1}{#2}{#3}{none}{none}}  


\newcommand{\bprefix}[3]{\kcell{#1}{#2}{$#3$}{convex}{none}}
\newcommand{\bsuffix}[3]{\kcell{#1}{#2}{$#3$}{none}{convex}}
\newcommand{\bmiddle}[3]{\kcell{#1}{#2}{$#3$}{none}{none}}
\newcommand{\bdot}{{\scriptscriptstyle\bullet}}
\newcommand{\bAnyVar}[1]{%
  \k@withTooltip{\mbox{--}}{Variable Sort: #1}%
}

\tikzset{
  cell/.style={
    line width=1pt,
    draw=#1!50!black,
    shade,
    shading=axis,
    top color=#1!20,
    bottom color=#1!20!white!90!black,
  },
  body/.style={
    rounded rectangle,
    rounded rectangle arc length=180,
    minimum width=3em,
    minimum height=4ex,
    inner ysep=.3333em,
    inner xsep=.3333em
  },
  label/.style={
    rectangle,
    inner xsep=.5ex,
    inner ysep=.5ex,
    text depth=.15em,
%    font=\sffamily\footnotesize
  },
}


%%% The main bubble drawing method \kcell.

\pgfdeclarelayer{background}
\pgfsetlayers{background,main}

\newlength{\k@cellContentWidth}
\newlength{\k@cellContentHeight}
\newlength{\k@labelXShift}
\newlength{\k@ruptureStepSize}

% Cell drawing happens roughly as follows:
% 1) The cell content is placed in the image.
% 2) TikZ fits a 'rounded rectangle' node around the content.  This node, which
%    we call 'body' here, remains invisible; its anchors serve as reference points.
% 3) The label is placed on the top left of the cell body.
% 4) The cell outline is drawn and filled on the background layer, that is,
%    behind the already placed cell content.
% 5) Some vertical space is added around the whole drawing.
\newcommand{\kcell}[5]{\hbox{%
  \begingroup
  \def\cellColor{#1}%
  \def\cellLabel{\textsf{\footnotesize\strut #2}}% The strut ensures even label height.
  \def\cellContent{#3}%
  % Parameters #4 and #5 determine whether the west and east arc are curved
  % or straight ("whole" or "ruptured").

  \begin{tikzpicture}[baseline=(cell content.base)]
    \begin{scope}[inner sep=0pt,outer sep=0pt,anchor=base west]
      % Beside the cell content, also draw an empty node a bit wider than
      % the cell label.  That way, the cell body will always be wide enough
      % for the label.
      \path node (cell content) {\cellContent}
            node                {\phantom{\cellLabel}\hbox to 2em {}};
    \end{scope}
    % Determine the size of the cell content.
    \def\k@cellContentBBox{\pgfpointdiff{\pgfpointanchor{current bounding box}{south west}}
                                        {\pgfpointanchor{current bounding box}{north east}}}
    \pgfextractx{\k@cellContentWidth}{\k@cellContentBBox}%
    \pgfextracty{\k@cellContentHeight}{\k@cellContentBBox}%
    
    \begin{pgfonlayer}{background}
      \ifdraft{%
        \path (cell content.center)
              node (cell body) [body,
                                rectangle,
                                anchor=center,
                                text width=\k@cellContentWidth,
                                text height=\k@cellContentHeight] {};
      }{%
        % Let TikZ find the best rounded rectangle around the content.
        \path (cell content.center)
              node (cell body) [body,
                                anchor=center,
                                text width=\k@cellContentWidth,
                                text height=\k@cellContentHeight,
                                rounded rectangle west arc=#4,
                                rounded rectangle east arc=#5] {};
      }
    \end{pgfonlayer}

    % Place the cell label relative to the rounded rectangle.  If the left side
    % is straight, shift the label a little to the right to avoid an ugly
    % long vertical left side.
    \ifthenelse{\equal{#4}{convex}}{%
      \setlength{\k@labelXShift}{0pt}%
    }{
      \setlength{\k@labelXShift}{1ex}
    }%

    \path (cell body.north west)
          ++(\k@labelXShift,.6ex)
          node (cell label) [label,anchor=base west] {\cellLabel};

    % Finally, draw the background of the cell behind the content.
    \begin{pgfonlayer}{background}
      % Decide how to draw the cell's west and east side.
      \ifthenelse{\equal{#4}{convex}}{%
        \def\cellWestArc{ arc (90:270:\n4 and \n3) -- (cell body.south west) }%
      }{%
        \ifdraft{%
          \def\cellWestArc{ |- (cell body.south west) }
        }{%
          % This yields a rounded zig zag pattern (starting outward).
          \def\cellWestArc{ { [rounded corners=.25ex]
                              \foreach \signPrefix in {-,0,-,0,-,0,-,0} {%
                                -- ++(\signPrefix{}.75\k@ruptureStepSize,-\k@ruptureStepSize)}
                            }
                          }%
        }%
      }%
      \ifthenelse{\equal{#5}{convex}}{%
        \def\cellEastArc{ arc (-90:90:\n4 and \n3) }%
      }{%
        \ifdraft{%
          \def\cellEastArc{ -- (cell body.north east) }
        }{%
          \def\cellEastArc{ { [rounded corners=.25ex]
                              \foreach \signPrefix in {0,-,0,-,0,-,0,-} {%
                                -- ++(\signPrefix{}.75\k@ruptureStepSize,\k@ruptureStepSize)}
                            }
                          }%
        }%
      }%

      % Draw the cell outline
      \path[cell=\cellColor]
                    % Compute half of the body's height.  The value is the
                    % radius for the arced sides; it also determines the size
                    % of the zig zag pattern of ruptured sides.
                    let \p1 = (cell body.north east),
                        \p2 = (cell body.center),
                        \n3 = {\y1 - \y2},
                        \n4 = {\n3 / 3}
                    in
                    \pgfextra{%
                      \setlength{\k@ruptureStepSize}{\n3}%
                      \setlength{\k@ruptureStepSize}{.25\k@ruptureStepSize}%
                     }%
                     
                    % Draw counter-clock-wise, starting from the
                    % lower right corner.
                    (cell body.south east)

                    % Right
                    \cellEastArc

                    % Top
                    { [rounded corners=.2em]
                                  -| (cell label.north east)
                                  -- (cell label.north west)
                                  |- (cell body.north west)
                    }
                    % A little offset to the left for a more pleasant look
                    -- ++(-.2em,0pt)

                    % Left
                    \cellWestArc

                    % Bottom (just close the path)
                    -- cycle;
    \end{pgfonlayer}
    
    % Add extra space above and below the cell.
    \path[use as bounding box] (current bounding box.south west) ++(0,-.3333em)
                               rectangle (current bounding box.north east) ++(0,.3333em);
  \end{tikzpicture}%
  \endgroup
}}


% Rules and Equations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\when}[1]{%
  \hspace{2em} when \ensuremath{#1}%
  %\k@markPosition%
}

%%% Context

% Context.
\newcommand{\kcontext}[2]{\par%
  \text{\scshape context:} $#2$%
  %\k@markPosition%
  \bigskip%
}
% Conditional context.
\newcommand{\kccontext}[3]{\par%
  \text{\scshape context:} $#2$ %
  \when{#3}%
  \bigskip%
}

%%% Equations and structural rules.

\newcommand{\k@ruleLabel}[2]{%
  \ifthenelse{\equal{#1}{}}{\mbox{\scshape #2}}{\k@withTooltip{\mbox{\scshape #2}}{Rule Label: #1}}%
}

\newcommand{\kequation}[2]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{rule}\hspace{1em}$#2$%
  }%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\kcequation}[3]{\par\indent%
  \k@ruleLabel{#1}{rule}\hspace{1em}$#2$%
  \when{#3}
  %\k@markPosition%
  \bigskip%
}
\newcommand{\mequation}[3]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{macro}\hspace{1em}$#2 = #3$%
  }%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\cmequation}[4]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{equation}\hspace{1em}$#2 = #3$%
    \when{#4}%
  }%
  %\k@markPosition%
  \bigskip%
}

%%% Rules.

\newcommand{\krule}[3][]{%
  \par\indent\hbox{%
    #1%
    \k@ruleLabel{#2}{rule}\hspace{1em}$#3$%
  }%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\kcrule}[3]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{rule}\hspace{1em}$#2$%
    \when{#3}%
  }%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\kndrule}[2]{\par%
  \k@ruleLabel{#1}{non-det rule}%
  \par\indent\hbox{$#2$}%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\mrule}[3]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{rule}\hspace{1em}$#2 \Rightarrow #3$%
  }%
  %\k@markPosition%
  \bigskip%
}
\newcommand{\cmrule}[4]{%
  \par\indent\hbox{%
    \k@ruleLabel{#1}{rule}\hspace{1em}$#2 \Rightarrow #3$%
    \when{#4}%
  }%
  %\k@markPosition%
  \bigskip%
}


\makeatother

